(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(g(x)) → g(g(f(x)))
g(s(x)) → s(s(g(x)))
s(x) → h(0, x)
s(x) → h(x, 0)
f(0) → 0
s(s(s(0))) → f(s(0))
f(s(0)) → s(0)
h(f(x), g(x)) → f(s(x))
g(x) → h(h(h(h(x, x), x), x), x)
f(s(s(x))) → h(f(x), g(h(x, x)))
s(0) → r(0)
s(s(s(0))) → r(s(0))
r(s(0)) → s(0)
g(x) → r(x)
s(0) → p(0)
s(s(0)) → p(s(0))
p(s(0)) → 0
s(s(s(s(s(0))))) → p(s(s(0)))
p(s(s(0))) → s(s(s(0)))
h(p(x), g(x)) → p(s(x))
s(0) → k(0)
s(s(p(p(a)))) → s(k(p(a)))
s(k(p(a))) → p(p(a))
g(x) → k(x)
a → 0
s(h(r(k(p(x))), r(x))) → h(r(r(p(x))), k(x))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(g(z0)) → g(g(f(z0)))
f(0) → 0
f(s(0)) → s(0)
f(s(s(z0))) → h(f(z0), g(h(z0, z0)))
g(s(z0)) → s(s(g(z0)))
g(z0) → h(h(h(h(z0, z0), z0), z0), z0)
g(z0) → r(z0)
g(z0) → k(z0)
s(z0) → h(0, z0)
s(z0) → h(z0, 0)
s(s(s(0))) → f(s(0))
s(0) → r(0)
s(s(s(0))) → r(s(0))
s(0) → p(0)
s(s(0)) → p(s(0))
s(s(s(s(s(0))))) → p(s(s(0)))
s(0) → k(0)
s(s(p(p(a)))) → s(k(p(a)))
s(k(p(a))) → p(p(a))
s(h(r(k(p(z0))), r(z0))) → h(r(r(p(z0))), k(z0))
h(f(z0), g(z0)) → f(s(z0))
h(p(z0), g(z0)) → p(s(z0))
r(s(0)) → s(0)
p(s(0)) → 0
p(s(s(0))) → s(s(s(0)))
a → 0
Tuples:
F(g(z0)) → c(G(g(f(z0))), G(f(z0)), F(z0))
F(s(0)) → c2(S(0))
F(s(s(z0))) → c3(H(f(z0), g(h(z0, z0))), F(z0), G(h(z0, z0)), H(z0, z0))
G(s(z0)) → c4(S(s(g(z0))), S(g(z0)), G(z0))
G(z0) → c5(H(h(h(h(z0, z0), z0), z0), z0), H(h(h(z0, z0), z0), z0), H(h(z0, z0), z0), H(z0, z0))
G(z0) → c6(R(z0))
S(z0) → c8(H(0, z0))
S(z0) → c9(H(z0, 0))
S(s(s(0))) → c10(F(s(0)), S(0))
S(0) → c11(R(0))
S(s(s(0))) → c12(R(s(0)), S(0))
S(0) → c13(P(0))
S(s(0)) → c14(P(s(0)), S(0))
S(s(s(s(s(0))))) → c15(P(s(s(0))), S(s(0)), S(0))
S(s(p(p(a)))) → c17(S(k(p(a))), P(a), A)
S(k(p(a))) → c18(P(p(a)), P(a), A)
S(h(r(k(p(z0))), r(z0))) → c19(H(r(r(p(z0))), k(z0)), R(r(p(z0))), R(p(z0)), P(z0))
H(f(z0), g(z0)) → c20(F(s(z0)), S(z0))
H(p(z0), g(z0)) → c21(P(s(z0)), S(z0))
R(s(0)) → c22(S(0))
P(s(s(0))) → c24(S(s(s(0))), S(s(0)), S(0))
S tuples:
F(g(z0)) → c(G(g(f(z0))), G(f(z0)), F(z0))
F(s(0)) → c2(S(0))
F(s(s(z0))) → c3(H(f(z0), g(h(z0, z0))), F(z0), G(h(z0, z0)), H(z0, z0))
G(s(z0)) → c4(S(s(g(z0))), S(g(z0)), G(z0))
G(z0) → c5(H(h(h(h(z0, z0), z0), z0), z0), H(h(h(z0, z0), z0), z0), H(h(z0, z0), z0), H(z0, z0))
G(z0) → c6(R(z0))
S(z0) → c8(H(0, z0))
S(z0) → c9(H(z0, 0))
S(s(s(0))) → c10(F(s(0)), S(0))
S(0) → c11(R(0))
S(s(s(0))) → c12(R(s(0)), S(0))
S(0) → c13(P(0))
S(s(0)) → c14(P(s(0)), S(0))
S(s(s(s(s(0))))) → c15(P(s(s(0))), S(s(0)), S(0))
S(s(p(p(a)))) → c17(S(k(p(a))), P(a), A)
S(k(p(a))) → c18(P(p(a)), P(a), A)
S(h(r(k(p(z0))), r(z0))) → c19(H(r(r(p(z0))), k(z0)), R(r(p(z0))), R(p(z0)), P(z0))
H(f(z0), g(z0)) → c20(F(s(z0)), S(z0))
H(p(z0), g(z0)) → c21(P(s(z0)), S(z0))
R(s(0)) → c22(S(0))
P(s(s(0))) → c24(S(s(s(0))), S(s(0)), S(0))
K tuples:none
Defined Rule Symbols:
f, g, s, h, r, p, a
Defined Pair Symbols:
F, G, S, H, R, P
Compound Symbols:
c, c2, c3, c4, c5, c6, c8, c9, c10, c11, c12, c13, c14, c15, c17, c18, c19, c20, c21, c22, c24
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
F(g(z0)) → c(G(g(f(z0))), G(f(z0)), F(z0))
F(s(0)) → c2(S(0))
F(s(s(z0))) → c3(H(f(z0), g(h(z0, z0))), F(z0), G(h(z0, z0)), H(z0, z0))
G(s(z0)) → c4(S(s(g(z0))), S(g(z0)), G(z0))
S(s(s(0))) → c10(F(s(0)), S(0))
S(s(s(0))) → c12(R(s(0)), S(0))
S(s(0)) → c14(P(s(0)), S(0))
S(s(s(s(s(0))))) → c15(P(s(s(0))), S(s(0)), S(0))
S(s(p(p(a)))) → c17(S(k(p(a))), P(a), A)
S(k(p(a))) → c18(P(p(a)), P(a), A)
S(h(r(k(p(z0))), r(z0))) → c19(H(r(r(p(z0))), k(z0)), R(r(p(z0))), R(p(z0)), P(z0))
H(f(z0), g(z0)) → c20(F(s(z0)), S(z0))
H(p(z0), g(z0)) → c21(P(s(z0)), S(z0))
R(s(0)) → c22(S(0))
P(s(s(0))) → c24(S(s(s(0))), S(s(0)), S(0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(g(z0)) → g(g(f(z0)))
f(0) → 0
f(s(0)) → s(0)
f(s(s(z0))) → h(f(z0), g(h(z0, z0)))
g(s(z0)) → s(s(g(z0)))
g(z0) → h(h(h(h(z0, z0), z0), z0), z0)
g(z0) → r(z0)
g(z0) → k(z0)
s(z0) → h(0, z0)
s(z0) → h(z0, 0)
s(s(s(0))) → f(s(0))
s(0) → r(0)
s(s(s(0))) → r(s(0))
s(0) → p(0)
s(s(0)) → p(s(0))
s(s(s(s(s(0))))) → p(s(s(0)))
s(0) → k(0)
s(s(p(p(a)))) → s(k(p(a)))
s(k(p(a))) → p(p(a))
s(h(r(k(p(z0))), r(z0))) → h(r(r(p(z0))), k(z0))
h(f(z0), g(z0)) → f(s(z0))
h(p(z0), g(z0)) → p(s(z0))
r(s(0)) → s(0)
p(s(0)) → 0
p(s(s(0))) → s(s(s(0)))
a → 0
Tuples:
G(z0) → c5(H(h(h(h(z0, z0), z0), z0), z0), H(h(h(z0, z0), z0), z0), H(h(z0, z0), z0), H(z0, z0))
G(z0) → c6(R(z0))
S(z0) → c8(H(0, z0))
S(z0) → c9(H(z0, 0))
S(0) → c11(R(0))
S(0) → c13(P(0))
S tuples:
G(z0) → c5(H(h(h(h(z0, z0), z0), z0), z0), H(h(h(z0, z0), z0), z0), H(h(z0, z0), z0), H(z0, z0))
G(z0) → c6(R(z0))
S(z0) → c8(H(0, z0))
S(z0) → c9(H(z0, 0))
S(0) → c11(R(0))
S(0) → c13(P(0))
K tuples:none
Defined Rule Symbols:
f, g, s, h, r, p, a
Defined Pair Symbols:
G, S
Compound Symbols:
c5, c6, c8, c9, c11, c13
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 6 of 6 dangling nodes:
G(z0) → c5(H(h(h(h(z0, z0), z0), z0), z0), H(h(h(z0, z0), z0), z0), H(h(z0, z0), z0), H(z0, z0))
G(z0) → c6(R(z0))
S(z0) → c8(H(0, z0))
S(z0) → c9(H(z0, 0))
S(0) → c11(R(0))
S(0) → c13(P(0))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(g(z0)) → g(g(f(z0)))
f(0) → 0
f(s(0)) → s(0)
f(s(s(z0))) → h(f(z0), g(h(z0, z0)))
g(s(z0)) → s(s(g(z0)))
g(z0) → h(h(h(h(z0, z0), z0), z0), z0)
g(z0) → r(z0)
g(z0) → k(z0)
s(z0) → h(0, z0)
s(z0) → h(z0, 0)
s(s(s(0))) → f(s(0))
s(0) → r(0)
s(s(s(0))) → r(s(0))
s(0) → p(0)
s(s(0)) → p(s(0))
s(s(s(s(s(0))))) → p(s(s(0)))
s(0) → k(0)
s(s(p(p(a)))) → s(k(p(a)))
s(k(p(a))) → p(p(a))
s(h(r(k(p(z0))), r(z0))) → h(r(r(p(z0))), k(z0))
h(f(z0), g(z0)) → f(s(z0))
h(p(z0), g(z0)) → p(s(z0))
r(s(0)) → s(0)
p(s(0)) → 0
p(s(s(0))) → s(s(s(0)))
a → 0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
f, g, s, h, r, p, a
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))